$k$(v) sends [${\it tg}$,$f$(State(${\it ds}$), v)] on $l$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Rsends(${\it ds}$;$k$;$A$;$l$;${\it tg}$ : $T$;[$<$${\it tg}$, $\lambda$$s$,$v$. [($f$($s$,$v$))]$>$])